<!DOCTYPE html>
<html class="client-nojs vector-feature-night-mode-disabled vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-sticky-header-enabled" lang="en" dir="ltr"><head>
<meta charset="UTF-8">
<title>Rule of replacement</title>
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<link rel="canonical" href="https://en.wikipedia.org/wiki/Rule_of_replacement"> <link href="./mw/ext.cite.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/ext.math.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.icons.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.search.codex.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/user.styles.css" rel="stylesheet" type="text/css">
<meta name="ResourceLoaderDynamicStyles" content="">
<link rel="stylesheet" type="text/css" href="./mw/site.styles.css">
<link rel="stylesheet" type="text/css" href="./mw/noscript.css">
<link rel="stylesheet" type="text/css" href="./footer.css">
<link rel="stylesheet" type="text/css" href="./vector-2022.css">
</head>
<body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject page-Rule_of_replacement rootpage-Rule_of_replacement skin-vector-2022 action-view">
<div class="mw-page-container">
<div class="mw-page-container-inner">
<div class="mw-content-container">
<main id="content" class="mw-body">
<header class="mw-body-header vector-page-titlebar">
<h1 id="firstHeading" class="firstHeading mw-first-heading">
<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Rule of replacement</span></span>
</h1>
</header>
<a id="top"></a>
<div id="bodyContent" class="vector-body ve-init-mw-desktopArticleTarget-targetContainer" aria-labelledby="firstHeading" data-mw-ve-target-container="">
<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="en" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr">
<style data-mw-deduplicate="TemplateStyles:r1129693374">
/* start https://en.wikipedia.org/ */
.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}
/* end https://en.wikipedia.org/ */
</style><style data-mw-deduplicate="TemplateStyles:r1126788409">
/* start https://en.wikipedia.org/ */
.mw-parser-output .plainlist ol,.mw-parser-output .plainlist ul{line-height:inherit;list-style:none;margin:0;padding:0}.mw-parser-output .plainlist ol li,.mw-parser-output .plainlist ul li{margin-bottom:0}
/* end https://en.wikipedia.org/ */
</style><style data-mw-deduplicate="TemplateStyles:r1246091330">
/* start https://en.wikipedia.org/ */
.mw-parser-output .sidebar{width:22em;float:right;clear:right;margin:0.5em 0 1em 1em;background:var(--background-color-neutral-subtle,#f8f9fa);border:1px solid var(--border-color-base,#a2a9b1);padding:0.2em;text-align:center;line-height:1.4em;font-size:88%;border-collapse:collapse;display:table}body.skin-minerva .mw-parser-output .sidebar{display:table!important;float:right!important;margin:0.5em 0 1em 1em!important}.mw-parser-output .sidebar-subgroup{width:100%;margin:0;border-spacing:0}.mw-parser-output .sidebar-left{float:left;clear:left;margin:0.5em 1em 1em 0}.mw-parser-output .sidebar-none{float:none;clear:both;margin:0.5em 1em 1em 0}.mw-parser-output .sidebar-outer-title{padding:0 0.4em 0.2em;font-size:125%;line-height:1.2em;font-weight:bold}.mw-parser-output .sidebar-top-image{padding:0.4em}.mw-parser-output .sidebar-top-caption,.mw-parser-output .sidebar-pretitle-with-top-image,.mw-parser-output .sidebar-caption{padding:0.2em 0.4em 0;line-height:1.2em}.mw-parser-output .sidebar-pretitle{padding:0.4em 0.4em 0;line-height:1.2em}.mw-parser-output .sidebar-title,.mw-parser-output .sidebar-title-with-pretitle{padding:0.2em 0.8em;font-size:145%;line-height:1.2em}.mw-parser-output .sidebar-title-with-pretitle{padding:0.1em 0.4em}.mw-parser-output .sidebar-image{padding:0.2em 0.4em 0.4em}.mw-parser-output .sidebar-heading{padding:0.1em 0.4em}.mw-parser-output .sidebar-content{padding:0 0.5em 0.4em}.mw-parser-output .sidebar-content-with-subgroup{padding:0.1em 0.4em 0.2em}.mw-parser-output .sidebar-above,.mw-parser-output .sidebar-below{padding:0.3em 0.8em;font-weight:bold}.mw-parser-output .sidebar-collapse .sidebar-above,.mw-parser-output .sidebar-collapse .sidebar-below{border-top:1px solid #aaa;border-bottom:1px solid #aaa}.mw-parser-output .sidebar-navbar{text-align:right;font-size:115%;padding:0 0.4em 0.4em}.mw-parser-output .sidebar-list-title{padding:0 0.4em;text-align:left;font-weight:bold;line-height:1.6em;font-size:105%}.mw-parser-output .sidebar-list-title-c{padding:0 0.4em;text-align:center;margin:0 3.3em}@media(max-width:640px){body.mediawiki .mw-parser-output .sidebar{width:100%!important;clear:both;float:none!important;margin-left:0!important;margin-right:0!important}}body.skin--responsive .mw-parser-output .sidebar a>img{max-width:none!important}@media screen{html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-list-title,html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle{background:transparent!important}html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle a{color:var(--color-progressive)!important}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-list-title,html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle{background:transparent!important}html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle a{color:var(--color-progressive)!important}}@media print{body.ns-0 .mw-parser-output .sidebar{display:none!important}}
/* end https://en.wikipedia.org/ */
</style><table class="sidebar nomobile nowraplinks plainlist"><tbody><tr><th class="sidebar-title"><a href="Rule_of_inference" title="Rule of inference">Transformation rules</a></th></tr><tr><th class="sidebar-heading" style="background:#eaeaff;;background:#ddf;font-size:110%; border-bottom:1px #fefefe solid;">
<a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">Propositional calculus</a></th></tr><tr><th class="sidebar-heading" style="background:#eaeaff;">
<a href="Rule_of_inference" title="Rule of inference">Rules of inference</a> (<a href="List_of_rules_of_inference" title="List of rules of inference">List</a>)</th></tr><tr><td class="sidebar-content" style="padding-top:0.15em;">
<ul><li><a href="Conditional_proof" title="Conditional proof"><span>Implication introduction</span></a> / <a href="Modus_ponens" title="Modus ponens"><span title="A→B, A ⊢ B">elimination (<i>modus ponens</i>)</span></a></li>
<li><a href="Biconditional_introduction" title="Biconditional introduction"><span title="A→B, B→A ⊢ A↔B">Biconditional introduction</span></a> / <a href="Biconditional_elimination" title="Biconditional elimination"><span title="A↔B ⊢ A→B">elimination</span></a></li>
<li><a href="Conjunction_introduction" title="Conjunction introduction"><span title="A, B ⊢ A∧B">Conjunction introduction</span></a> / <a href="Conjunction_elimination" title="Conjunction elimination"><span title="A∧B ⊢ A">elimination</span></a></li>
<li><a href="Disjunction_introduction" title="Disjunction introduction"><span title="A ⊢ A∨B">Disjunction introduction</span></a> / <a href="Disjunction_elimination" title="Disjunction elimination"><span title="A∨B, A→C, B→C ⊢ C">elimination</span></a></li>
<li><a href="Disjunctive_syllogism" title="Disjunctive syllogism"><span title="A∨B, ¬A ⊢ B">Disjunctive</span></a> / <a href="Hypothetical_syllogism" title="Hypothetical syllogism"><span title="A→B, B→C ⊢ A→C">hypothetical syllogism</span></a></li>
<li><a href="Constructive_dilemma" title="Constructive dilemma"><span title="A→P, B→Q, A∨B ⊢ P∨Q">Constructive</span></a> / <a href="Destructive_dilemma" title="Destructive dilemma"><span title="A→P, B→Q, ¬P∨¬Q ⊢ ¬A∨¬B">destructive dilemma</span></a></li>
<li><a href="Absorption_(logic)" title="Absorption (logic)"><span title="A→B ⊢ A→A∧B">Absorption</span></a> / <a href="Modus_tollens" title="Modus tollens"><span title="A→B, ¬B ⊢ ¬A"><i>modus tollens</i></span></a> / <a href="Modus_ponendo_tollens" title="Modus ponendo tollens"><span title="¬(A∧B), A ⊢ ¬B"><i>modus ponendo tollens</i></span></a></li>
<li><a href="Modus_non_excipiens" title="Modus non excipiens">Modus non excipiens</a></li>
<li><a href="Negation_introduction" title="Negation introduction">Negation introduction</a></li></ul></td>
</tr><tr><th class="sidebar-heading" style="background:#eaeaff;">
</th></tr><tr><td class="sidebar-content" style="padding-top:0.15em;">
<div class="hlist">
<ul><li><a href="Associative_property#Propositional_logic" title="Associative property"><span title="A∨(B∨C) = (A∨B)∨C">Associativity</span></a></li>
<li><a href="Commutative_property#Propositional_logic" title="Commutative property"><span title="A∨B = B∨A">Commutativity</span></a></li>
<li><a href="Distributive_property#Propositional_logic" title="Distributive property"><span title="A∧(B∨C) = (A∧B)∨(A∧C)">Distributivity</span></a></li>
<li><a href="Double_negation" title="Double negation"><span title="¬¬A = A">Double negation</span></a></li>
<li><a href="De_Morgan's_laws" title="De Morgan's laws">De Morgan's laws</a></li>
<li><a href="Transposition_(logic)" class="mw-redirect" title="Transposition (logic)">Transposition</a></li>
<li><a href="Material_implication_(rule_of_inference)" title="Material implication (rule of inference)"><span title="A→B ⊢ ¬A∨B">Material implication</span></a></li>
<li><a href="Exportation_(logic)" title="Exportation (logic)"><span title="(A∧B)→C ⊢ A→(B→C)">Exportation</span></a></li>
<li><a href="Tautology_(rule_of_inference)" title="Tautology (rule of inference)"><span title="A∨A = A">Tautology</span></a></li></ul>
</div></td>
</tr><tr><th class="sidebar-heading" style="background:#eaeaff;;background:#ddf;font-size:110%;">
<a href="First-order_logic" title="First-order logic">Predicate logic</a></th></tr><tr><th class="sidebar-heading" style="background:#eaeaff;">
<a href="Rule_of_inference" title="Rule of inference">Rules of inference</a></th></tr><tr><td class="sidebar-content" style="padding-top:0.15em;">
<ul><li><a href="Universal_generalization" title="Universal generalization">Universal generalization</a> / <a href="Universal_instantiation" title="Universal instantiation">instantiation</a></li>
<li><a href="Existential_generalization" title="Existential generalization">Existential generalization</a> / <a href="Existential_instantiation" title="Existential instantiation">instantiation</a></li></ul></td>
</tr><tr><td class="sidebar-navbar"><style data-mw-deduplicate="TemplateStyles:r1239400231">
/* start https://en.wikipedia.org/ */
.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}
/* end https://en.wikipedia.org/ */
</style></td></tr></tbody></table>
<p>In <a href="Logic" title="Logic">logic</a>, a <b>rule of replacement</b><sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> is a <a href="Transformation_rule" class="mw-redirect" title="Transformation rule">transformation rule</a> that may be applied to only a particular segment of an <a href="Well-formed_formula" title="Well-formed formula">expression</a>. A <a href="Logical_system" class="mw-redirect" title="Logical system">logical system</a> may be constructed so that it uses either <a href="Axiom" title="Axiom">axioms</a>, <a href="Rules_of_inference" class="mw-redirect" title="Rules of inference">rules of inference</a>, or both as transformation rules for <a href="Well-formed_formula" title="Well-formed formula">logical expressions</a> in the system. Whereas a rule of inference is always applied to a whole logical expression, a rule of replacement may be applied to only a particular segment. Within the context of a <a href="Logical_proof" class="mw-redirect" title="Logical proof">logical proof</a>, <a href="Logically_equivalent" class="mw-redirect" title="Logically equivalent">logically equivalent</a> expressions may replace each other. Rules of replacement are used in <a href="Propositional_logic" title="Propositional logic">propositional logic</a> to manipulate <a href="Proposition" title="Proposition">propositions</a>.
</p><p>Common rules of replacement include <a href="De_Morgan's_laws" title="De Morgan's laws">de Morgan's laws</a>, <a href="Commutative_property" title="Commutative property">commutation</a>, <a href="Associative_property" title="Associative property">association</a>, <a href="Distribution_(logic)" class="mw-redirect" title="Distribution (logic)">distribution</a>, <a href="Double_negation" title="Double negation">double negation</a>,<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>a<span class="cite-bracket">]</span></a></sup> <a href="Transposition_(logic)" class="mw-redirect" title="Transposition (logic)">transposition</a>, <a href="Material_implication_(rule_of_inference)" title="Material implication (rule of inference)">material implication</a>, <a href="Logical_equivalence" title="Logical equivalence">logical equivalence</a>, <a href="Exportation_(logic)" title="Exportation (logic)">exportation</a>, and <a href="Tautology_(rule_of_inference)" title="Tautology (rule of inference)">tautology</a>.
</p>
<meta property="mw:PageProp/toc">
<div class="mw-heading mw-heading2"><h2 id="Table:_Rules_of_Replacement">Table: Rules of Replacement</h2></div>
<p>The rules above can be summed up in the following table.<sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup> The "<a href="Tautology_(logic)" title="Tautology (logic)">Tautology</a>" column shows how to interpret the notation of a given rule.
</p>
<table class="wikitable">
<tbody><tr>
<th>Rules of inference
</th>
<th>Tautology
</th>
<th>Name
</th></tr>
<tr>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}(p\vee q)\vee r\\\therefore {\overline {p\vee (q\vee r)}}\\\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo>∨<!-- ∨ --></mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
<mo>∨<!-- ∨ --></mo>
<mi>r</mi>
</mtd>
</mtr>
<mtr>
<mtd>
<mo>∴<!-- ∴ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mi>p</mi>
<mo>∨<!-- ∨ --></mo>
<mo stretchy="false">(</mo>
<mi>q</mi>
<mo>∨<!-- ∨ --></mo>
<mi>r</mi>
<mo stretchy="false">)</mo>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}(p\vee q)\vee r\\\therefore {\overline {p\vee (q\vee r)}}\\\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./0141e10a72504ec1a042c8a1e2f2bc47bb24b87f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.838ex; width:13.324ex; height:6.843ex;" alt="{\displaystyle {\begin{aligned}(p\vee q)\vee r\\\therefore {\overline {p\vee (q\vee r)}}\\\end{aligned}}}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((p\vee q)\vee r)\rightarrow (p\vee (q\vee r))}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">(</mo>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo>∨<!-- ∨ --></mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
<mo>∨<!-- ∨ --></mo>
<mi>r</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">→<!-- → --></mo>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo>∨<!-- ∨ --></mo>
<mo stretchy="false">(</mo>
<mi>q</mi>
<mo>∨<!-- ∨ --></mo>
<mi>r</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle ((p\vee q)\vee r)\rightarrow (p\vee (q\vee r))}</annotation>
</semantics>
</math></span><img src="./482d8a774fbeaf3dc28d5ec4094d9b58a5b66fbe.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:27.757ex; height:2.843ex;" alt="{\displaystyle ((p\vee q)\vee r)\rightarrow (p\vee (q\vee r))}" loading="lazy"></span>
</td>
<td><a href="Associative_property#Propositional_logic" title="Associative property">Associative</a>
</td></tr>
<tr>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}p\wedge q\\\therefore {\overline {q\wedge p}}\\\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd>
<mi>p</mi>
<mo>∧<!-- ∧ --></mo>
<mi>q</mi>
</mtd>
</mtr>
<mtr>
<mtd>
<mo>∴<!-- ∴ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mi>q</mi>
<mo>∧<!-- ∧ --></mo>
<mi>p</mi>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}p\wedge q\\\therefore {\overline {q\wedge p}}\\\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./4fca8ed6d1af319ec767d07e4152d7152bf4d442.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.505ex; width:7.883ex; height:6.176ex;" alt="{\displaystyle {\begin{aligned}p\wedge q\\\therefore {\overline {q\wedge p}}\\\end{aligned}}}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p\wedge q)\rightarrow (q\wedge p)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo>∧<!-- ∧ --></mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">→<!-- → --></mo>
<mo stretchy="false">(</mo>
<mi>q</mi>
<mo>∧<!-- ∧ --></mo>
<mi>p</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle (p\wedge q)\rightarrow (q\wedge p)}</annotation>
</semantics>
</math></span><img src="./e4b6f83ff4ae5c64a3ff166a4f8c07c59c5567e5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:16.876ex; height:2.843ex;" alt="{\displaystyle (p\wedge q)\rightarrow (q\wedge p)}" loading="lazy"></span>
</td>
<td><a href="Commutative_property#Propositional_logic" title="Commutative property">Commutative</a>
</td></tr>
<tr>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}(p\wedge q)\rightarrow r\\\therefore {\overline {p\rightarrow (q\rightarrow r)}}\\\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo>∧<!-- ∧ --></mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">→<!-- → --></mo>
<mi>r</mi>
</mtd>
</mtr>
<mtr>
<mtd>
<mo>∴<!-- ∴ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mi>p</mi>
<mo stretchy="false">→<!-- → --></mo>
<mo stretchy="false">(</mo>
<mi>q</mi>
<mo stretchy="false">→<!-- → --></mo>
<mi>r</mi>
<mo stretchy="false">)</mo>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}(p\wedge q)\rightarrow r\\\therefore {\overline {p\rightarrow (q\rightarrow r)}}\\\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./a9453a89c178c20a958fe368c934d696e709cda5.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.838ex; width:15.387ex; height:6.843ex;" alt="{\displaystyle {\begin{aligned}(p\wedge q)\rightarrow r\\\therefore {\overline {p\rightarrow (q\rightarrow r)}}\\\end{aligned}}}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((p\wedge q)\rightarrow r)\rightarrow (p\rightarrow (q\rightarrow r))}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">(</mo>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo>∧<!-- ∧ --></mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">→<!-- → --></mo>
<mi>r</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">→<!-- → --></mo>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo stretchy="false">→<!-- → --></mo>
<mo stretchy="false">(</mo>
<mi>q</mi>
<mo stretchy="false">→<!-- → --></mo>
<mi>r</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle ((p\wedge q)\rightarrow r)\rightarrow (p\rightarrow (q\rightarrow r))}</annotation>
</semantics>
</math></span><img src="./bc62e1cf55fcee505f4e92c31af12466a140dc18.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:30.851ex; height:2.843ex;" alt="{\displaystyle ((p\wedge q)\rightarrow r)\rightarrow (p\rightarrow (q\rightarrow r))}" loading="lazy"></span>
</td>
<td><a href="Exportation_(logic)" title="Exportation (logic)">Exportation</a>
</td></tr>
<tr>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}p\rightarrow q\\\therefore {\overline {\neg q\rightarrow \neg p}}\\\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd>
<mi>p</mi>
<mo stretchy="false">→<!-- → --></mo>
<mi>q</mi>
</mtd>
</mtr>
<mtr>
<mtd>
<mo>∴<!-- ∴ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>q</mi>
<mo stretchy="false">→<!-- → --></mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>p</mi>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}p\rightarrow q\\\therefore {\overline {\neg q\rightarrow \neg p}}\\\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./d8b9adc014b827cb1c58b5a4b9589ebd31dabb59.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.338ex; width:12.016ex; height:5.843ex;" alt="{\displaystyle {\begin{aligned}p\rightarrow q\\\therefore {\overline {\neg q\rightarrow \neg p}}\\\end{aligned}}}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p\rightarrow q)\rightarrow (\neg q\rightarrow \neg p)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo stretchy="false">→<!-- → --></mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">→<!-- → --></mo>
<mo stretchy="false">(</mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>q</mi>
<mo stretchy="false">→<!-- → --></mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>p</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle (p\rightarrow q)\rightarrow (\neg q\rightarrow \neg p)}</annotation>
</semantics>
</math></span><img src="./5b37d9f299a4298239f4eaf69aec38361b24e68e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:22.039ex; height:2.843ex;" alt="{\displaystyle (p\rightarrow q)\rightarrow (\neg q\rightarrow \neg p)}" loading="lazy"></span>
</td>
<td><a href="Transposition_(logic)" class="mw-redirect" title="Transposition (logic)">Transposition or contraposition law</a>
</td></tr>
<tr>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}p\rightarrow q\\\therefore {\overline {\neg p\vee q}}\\\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd>
<mi>p</mi>
<mo stretchy="false">→<!-- → --></mo>
<mi>q</mi>
</mtd>
</mtr>
<mtr>
<mtd>
<mo>∴<!-- ∴ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>p</mi>
<mo>∨<!-- ∨ --></mo>
<mi>q</mi>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}p\rightarrow q\\\therefore {\overline {\neg p\vee q}}\\\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./77cf73ab67588e93b2f85f203ce473ddb2d6e451.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.505ex; width:9.455ex; height:6.176ex;" alt="{\displaystyle {\begin{aligned}p\rightarrow q\\\therefore {\overline {\neg p\vee q}}\\\end{aligned}}}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p\rightarrow q)\rightarrow (\neg p\vee q)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo stretchy="false">→<!-- → --></mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">→<!-- → --></mo>
<mo stretchy="false">(</mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>p</mi>
<mo>∨<!-- ∨ --></mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle (p\rightarrow q)\rightarrow (\neg p\vee q)}</annotation>
</semantics>
</math></span><img src="./3f60c2e786486b431a16c653e6ba228a71dd326f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:19.458ex; height:2.843ex;" alt="{\displaystyle (p\rightarrow q)\rightarrow (\neg p\vee q)}" loading="lazy"></span>
</td>
<td><a href="Material_implication_(rule_of_inference)" title="Material implication (rule of inference)">Material implication</a>
</td></tr>
<tr>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}(p\vee q)\wedge r\\\therefore {\overline {(p\wedge r)\vee (q\wedge r)}}\\\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo>∨<!-- ∨ --></mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
<mo>∧<!-- ∧ --></mo>
<mi>r</mi>
</mtd>
</mtr>
<mtr>
<mtd>
<mo>∴<!-- ∴ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo>∧<!-- ∧ --></mo>
<mi>r</mi>
<mo stretchy="false">)</mo>
<mo>∨<!-- ∨ --></mo>
<mo stretchy="false">(</mo>
<mi>q</mi>
<mo>∧<!-- ∧ --></mo>
<mi>r</mi>
<mo stretchy="false">)</mo>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}(p\vee q)\wedge r\\\therefore {\overline {(p\wedge r)\vee (q\wedge r)}}\\\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./181885d3de61a0bf31512de43e37a9cdc86786ba.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.838ex; width:18.765ex; height:6.843ex;" alt="{\displaystyle {\begin{aligned}(p\vee q)\wedge r\\\therefore {\overline {(p\wedge r)\vee (q\wedge r)}}\\\end{aligned}}}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((p\vee q)\wedge r)\rightarrow ((p\wedge r)\vee (q\wedge r))}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">(</mo>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo>∨<!-- ∨ --></mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
<mo>∧<!-- ∧ --></mo>
<mi>r</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">→<!-- → --></mo>
<mo stretchy="false">(</mo>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo>∧<!-- ∧ --></mo>
<mi>r</mi>
<mo stretchy="false">)</mo>
<mo>∨<!-- ∨ --></mo>
<mo stretchy="false">(</mo>
<mi>q</mi>
<mo>∧<!-- ∧ --></mo>
<mi>r</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle ((p\vee q)\wedge r)\rightarrow ((p\wedge r)\vee (q\wedge r))}</annotation>
</semantics>
</math></span><img src="./f2cff986517b87dd8614570474b5fc954692422c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:33.197ex; height:2.843ex;" alt="{\displaystyle ((p\vee q)\wedge r)\rightarrow ((p\wedge r)\vee (q\wedge r))}" loading="lazy"></span>
</td>
<td><a href="Distributive_property#Propositional_logic" title="Distributive property">Distributive</a>
</td></tr>
<tr>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}p\\q\\\therefore {\overline {p\wedge q}}\\\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd>
<mi>p</mi>
</mtd>
</mtr>
<mtr>
<mtd>
<mi>q</mi>
</mtd>
</mtr>
<mtr>
<mtd>
<mo>∴<!-- ∴ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mi>p</mi>
<mo>∧<!-- ∧ --></mo>
<mi>q</mi>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}p\\q\\\therefore {\overline {p\wedge q}}\\\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./6f491b93b4782661f0a96bb9f7a9476dd4dbe041.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -4.005ex; width:7.905ex; height:9.176ex;" alt="{\displaystyle {\begin{aligned}p\\q\\\therefore {\overline {p\wedge q}}\\\end{aligned}}}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle ((p)\wedge (q))\rightarrow (p\wedge q)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">(</mo>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo stretchy="false">)</mo>
<mo>∧<!-- ∧ --></mo>
<mo stretchy="false">(</mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">)</mo>
<mo stretchy="false">→<!-- → --></mo>
<mo stretchy="false">(</mo>
<mi>p</mi>
<mo>∧<!-- ∧ --></mo>
<mi>q</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle ((p)\wedge (q))\rightarrow (p\wedge q)}</annotation>
</semantics>
</math></span><img src="./6462d2bb765362c23a0b7dc5feac8d94d5488c51.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:20.494ex; height:2.843ex;" alt="{\displaystyle ((p)\wedge (q))\rightarrow (p\wedge q)}" loading="lazy"></span>
</td>
<td><a href="Logical_conjunction" title="Logical conjunction">Conjunction</a>
</td></tr>
<tr>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}p\\\therefore {\overline {\neg \neg p}}\\\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd>
<mi>p</mi>
</mtd>
</mtr>
<mtr>
<mtd>
<mo>∴<!-- ∴ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mrow>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>p</mi>
</mrow>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}p\\\therefore {\overline {\neg \neg p}}\\\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./9cd73c79ef971f1378fa59ee971a3d9bfc1a097f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.338ex; width:7.332ex; height:5.843ex;" alt="{\displaystyle {\begin{aligned}p\\\therefore {\overline {\neg \neg p}}\\\end{aligned}}}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p\rightarrow (\neg \neg p)}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mi>p</mi>
<mo stretchy="false">→<!-- → --></mo>
<mo stretchy="false">(</mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>p</mi>
<mo stretchy="false">)</mo>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle p\rightarrow (\neg \neg p)}</annotation>
</semantics>
</math></span><img src="./51b7354013e157dc44005592cbfacfcdaf3c0f6c.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; margin-left: -0.089ex; width:10.952ex; height:2.843ex;" alt="{\displaystyle p\rightarrow (\neg \neg p)}" loading="lazy"></span>
</td>
<td><a href="Double_negation" title="Double negation">Double negation introduction</a>
</td></tr>
<tr>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\begin{aligned}{\neg \neg p}\\\therefore {\overline {p}}\\\end{aligned}}}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mrow class="MJX-TeXAtom-ORD">
<mtable columnalign="right left right left right left right left right left right left" rowspacing="3pt" columnspacing="0em 2em 0em 2em 0em 2em 0em 2em 0em 2em 0em" displaystyle="true">
<mtr>
<mtd>
<mrow class="MJX-TeXAtom-ORD">
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>p</mi>
</mrow>
</mtd>
</mtr>
<mtr>
<mtd>
<mo>∴<!-- ∴ --></mo>
<mrow class="MJX-TeXAtom-ORD">
<mover>
<mi>p</mi>
<mo accent="false">¯<!-- ¯ --></mo>
</mover>
</mrow>
</mtd>
</mtr>
</mtable>
</mrow>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle {\begin{aligned}{\neg \neg p}\\\therefore {\overline {p}}\\\end{aligned}}}</annotation>
</semantics>
</math></span><img src="./0cef4a560617b2e6486720e67ba7ffd39664cf1f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -2.338ex; width:5.022ex; height:5.843ex;" alt="{\displaystyle {\begin{aligned}{\neg \neg p}\\\therefore {\overline {p}}\\\end{aligned}}}" loading="lazy"></span>
</td>
<td><span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (\neg \neg p)\rightarrow p}">
<semantics>
<mrow class="MJX-TeXAtom-ORD">
<mstyle displaystyle="true" scriptlevel="0">
<mo stretchy="false">(</mo>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi mathvariant="normal">¬<!-- ¬ --></mi>
<mi>p</mi>
<mo stretchy="false">)</mo>
<mo stretchy="false">→<!-- → --></mo>
<mi>p</mi>
</mstyle>
</mrow>
<annotation encoding="application/x-tex">{\displaystyle (\neg \neg p)\rightarrow p}</annotation>
</semantics>
</math></span><img src="./4637e515dd31fdbd884a4e1d8742aa222d6da392.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:10.863ex; height:2.843ex;" alt="{\displaystyle (\neg \neg p)\rightarrow p}" loading="lazy"></span>
</td>
<td><a href="Double_negation_elimination" class="mw-redirect" title="Double negation elimination">Double negation elimination</a>
</td></tr></tbody></table>
<div class="mw-heading mw-heading2"><h2 id="See_also">See also</h2></div>
<ul><li><i><a href="Salva_veritate" title="Salva veritate">Salva veritate</a></i></li></ul>
<div class="mw-heading mw-heading2"><h2 id="Notes">Notes</h2></div>
<style data-mw-deduplicate="TemplateStyles:r1239543626">
/* start https://en.wikipedia.org/ */
.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}
/* end https://en.wikipedia.org/ */
</style><div class="reflist reflist-lower-alpha">
<div class="mw-references-wrap"><ol class="references">
<li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text">not admitted in <a href="Intuitionistic_logic" title="Intuitionistic logic">intuitionistic logic</a></span>
</li>
</ol></div></div>
<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>
<div class="reflist">
<div class="mw-references-wrap"><ol class="references">
<li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text"><style data-mw-deduplicate="TemplateStyles:r1238218222">
/* start https://en.wikipedia.org/ */
.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}
/* end https://en.wikipedia.org/ */
</style><cite id="CITEREFCopiCohen2005" class="citation book cs1">Copi, Irving M.; Cohen, Carl (2005). <i>Introduction to Logic</i>. Prentice Hall.</cite></span>
</li>
<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text"><cite id="CITEREFHurley1991" class="citation book cs1">Hurley, Patrick (1991). <span class="id-lock-registration" title="Free registration required"><a rel="nofollow" class="external text" href="https://archive.org/details/studyguidetoacco00burc"><i>A Concise Introduction to Logic 4th edition</i></a></span>. Wadsworth Publishing. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9780534145156</bdi>.</cite></span>
</li>
<li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text">Moore and Parker </span>
</li>
<li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text">Kenneth H. Rosen: <i>Discrete Mathematics and its Applications</i>, Fifth Edition, p. 58.</span>
</li>
</ol></div></div>
<p><br>
</p>
<style data-mw-deduplicate="TemplateStyles:r1271159938">
/* start https://en.wikipedia.org/ */
.mw-parser-output .asbox{position:relative;overflow:hidden}.mw-parser-output .asbox table{background:transparent}.mw-parser-output .asbox p{margin:0}.mw-parser-output .asbox p+p{margin-top:0.25em}.mw-parser-output .asbox-body{font-style:italic}.mw-parser-output .asbox-note{font-size:smaller}.mw-parser-output .asbox .navbar{position:absolute;top:-0.75em;right:1em;display:none}.mw-parser-output :not(p):not(.asbox)+style+.asbox,.mw-parser-output :not(p):not(.asbox)+link+.asbox{margin-top:3em}
/* end https://en.wikipedia.org/ */
</style></div><!--htdig_noindex--><div><div class="zim-footer">
This article is issued from <a class="external text" title="Last edited on 2025-03-03" href="https://en.wikipedia.org/wiki/?title=Rule_of_replacement&oldid=1278551049">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.
</div>
</div><!--/htdig_noindex--></div>
</div>
</main>
</div>
</div>
</div>
</body></html>